D:Dsys, dec:(j,b:IdM(j).state(M(j).da(locl(b))+Unit)). d-chooser(D;dec)  Prop 

latex

Definitions	Dsys, t  T, Unit, Type, x:A. B(x), locl(a), M(i), M.da(a), left+right, M.state, x:AB(x), Id, f(a), P  Q, outl(x), M.pre(a,s,v), a in dom(M.pre), Prop, A & B, isl(x), b, x:AB(x), x:A. B(x), P  Q, P & Q, d-chooser(D;dec)
Lemmas	iff wf, assert wf, isl wf, ma-has-pre wf, ma-pre wf, outl wf, Id wf, ma-st wf, ma-da wf, d-m wf, locl wf, unit wf, dsys wf